Termination Proof Script

Consider the TRS R consisting of the rewrite rules


1:	app(app(map,f),nil)	→ nil
2:	app(app(map,f),app(app(cons,x),xs))	→ app(app(cons,app(f,x)),app(app(map,f),xs))
3:	app(app(app(comp,f),g),x)	→ app(f,app(g,x))
4:	app(twice,f)	→ app(app(comp,f),f)

There are 8 dependency pairs:


5:	APP(app(map,f),app(app(cons,x),xs))	→ APP(app(cons,app(f,x)),app(app(map,f),xs))
6:	APP(app(map,f),app(app(cons,x),xs))	→ APP(cons,app(f,x))
7:	APP(app(map,f),app(app(cons,x),xs))	→ APP(f,x)
8:	APP(app(map,f),app(app(cons,x),xs))	→ APP(app(map,f),xs)
9:	APP(app(app(comp,f),g),x)	→ APP(f,app(g,x))
10:	APP(app(app(comp,f),g),x)	→ APP(g,x)
11:	APP(twice,f)	→ APP(app(comp,f),f)
12:	APP(twice,f)	→ APP(comp,f)

The approximated dependency graph contains one SCC: {5,7-11}.

Tyrolean Termination Tool (0.07 seconds) --- May 3, 2006